Termination proof of /tmp/tmpUgv1

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇒)

↳2 JBCTerminationGraph

↳3 FIGtoITRSProof (⇒)

↳4 AND

    ↳5 IDP

        ↳6 IDPNonInfProof (⇒)

        ↳7 IDP

        ↳8 IDependencyGraphProof (⇔)

        ↳9 IDP

        ↳10 IDPNonInfProof (⇒)

        ↳11 IDP

        ↳12 IDependencyGraphProof (⇔)

        ↳13 TRUE

    ↳14 IDP

        ↳15 IDPNonInfProof (⇒)

        ↳16 AND

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔)

                ↳19 TRUE

            ↳20 IDP

                ↳21 IDependencyGraphProof (⇔)

                ↳22 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Sun Microsystems Inc.) Main-Class: CyclicList

/**
 * This class represents a list. The function get(n) can be used to access
 * the n-th element. 
 * @author Marc Brockschmidt
 */
public class CyclicList {
	/**
	 * A reference to the next list element.
	 */
	private CyclicList next;
	
	public static void main(String[] args) {
		CyclicList list = CyclicList.create(args.length);
		list.get(args[0].length());
	}
	
	/**
	 * Create a new list element.
	 * @param n a reference to the next element.
	 */
	public CyclicList(final CyclicList n) {
		this.next = n;
	}
	
	/**
	 * Create a new cyclical list of a length l.
	 * @param l some length
	 * @return cyclical list of length max(1, l)
	 */
	public static CyclicList create(int x) {
		CyclicList last, current;
		last = current = new CyclicList(null);
		while (--x > 0)
			current = new CyclicList(current);
		return last.next = current;
	}

	public CyclicList get(int n) {
		CyclicList cur = this;
		while (--n > 0) {
			cur = cur.next;
		}
		return cur;
	}	
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
CyclicList.main([Ljava/lang/String;)V: Graph of 157 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 24 rules for P and 27 rules for R.

Combined rules. Obtained 4 rules for P and 0 rules for R.

Filtered ground terms:

CyclicList(x1, x2) → CyclicList(x2)
567_0_get_Load(x1, x2, x3) → 567_0_get_Load(x2, x3)
Cond_567_1_main_InvokeMethod3(x1, x2, x3) → Cond_567_1_main_InvokeMethod3(x1, x2)

Combined rules. Obtained 4 rules for P and 0 rules for R.

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.

Log for SCC 1:

Generated 17 rules for P and 122 rules for R.

Combined rules. Obtained 1 rules for P and 0 rules for R.

Filtered ground terms:

CyclicList(x1) → CyclicList
160_0_create_Load(x1, x2, x3, x4) → 160_0_create_Load(x2, x4)

Combined rules. Obtained 1 rules for P and 0 rules for R.

Finished conversion. Obtained 1 rules for P and 0 rules for R. System has predefined symbols.

(4) Complex Obligation (AND)

(5) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(x0[0] > 0, 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))
(1): COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[1] + -1, x3[1]), java.lang.Object(x2[1]))
(2): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(x0[2] > 0, 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
(3): COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
(4): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(x0[4] > 0, 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
(5): COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[5] + -1, x2[5]), java.lang.Object(CyclicList(x1[5])))
(6): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(x0[6] > 0, 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))
(7): COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

(0) -> (1), if ((x0[0] > 0 →^* TRUE)∧(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))) →^* 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))))∧(java.lang.Object(x2[0]) →^* java.lang.Object(x2[1])))

(1) -> (0), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(x2[0])))

(1) -> (2), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(x1[2])))

(1) -> (4), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(CyclicList(x1[4]))))

(1) -> (6), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(CyclicList(java.lang.Object(EOR)))))

(2) -> (3), if ((x0[2] > 0 →^* TRUE)∧(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[2]) →^* java.lang.Object(x1[3])))

(3) -> (0), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x1[3]) →^* java.lang.Object(x2[0])))

(3) -> (2), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[3]) →^* java.lang.Object(x1[2])))

(3) -> (4), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x1[3]) →^* java.lang.Object(CyclicList(x1[4]))))

(3) -> (6), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[3]) →^* java.lang.Object(CyclicList(java.lang.Object(EOR)))))

(4) -> (5), if ((x0[4] > 0 →^* TRUE)∧(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))) →^* 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))))∧(java.lang.Object(CyclicList(x1[4])) →^* java.lang.Object(CyclicList(x1[5]))))

(5) -> (0), if ((567_0_get_Load(x0[5] + -1, x2[5]) →^* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(CyclicList(x1[5])) →^* java.lang.Object(x2[0])))

(5) -> (2), if ((567_0_get_Load(x0[5] + -1, x2[5]) →^* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(CyclicList(x1[5])) →^* java.lang.Object(x1[2])))

(5) -> (4), if ((567_0_get_Load(x0[5] + -1, x2[5]) →^* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(CyclicList(x1[5])) →^* java.lang.Object(CyclicList(x1[4]))))

(5) -> (6), if ((567_0_get_Load(x0[5] + -1, x2[5]) →^* 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(CyclicList(x1[5])) →^* java.lang.Object(CyclicList(java.lang.Object(EOR)))))

(6) -> (7), if ((x0[6] > 0 →^* TRUE)∧(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR))))))

(7) -> (0), if ((567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(CyclicList(java.lang.Object(EOR))) →^* java.lang.Object(x2[0])))

(7) -> (2), if ((567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(CyclicList(java.lang.Object(EOR))) →^* java.lang.Object(x1[2])))

(7) -> (4), if ((567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(CyclicList(java.lang.Object(EOR))) →^* java.lang.Object(CyclicList(x1[4]))))

(7) -> (6), if (567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →^* 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))))

The set Q is empty.

(6) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) → COND_567_1_MAIN_INVOKEMETHOD(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) the following chains were created:

We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])), COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) which results in the following constraint:
(1)    (>(x0[0], 0)=TRUE∧567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0])))=567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1])))∧java.lang.Object(x2[0])=java.lang.Object(x2[1]) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (>(x0[0], 0)=TRUE ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[0] + [bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[0] + [bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[0] + [bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)bni_16] = 0∧0 = 0∧[(-1)Bound*bni_16] + [bni_16]x0[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)bni_16] = 0∧0 = 0∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x0[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), x3), java.lang.Object(x2)) the following chains were created:

We consider the chain COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) which results in the following constraint:
(8)    (COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1]))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1]))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))∧(U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(12)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) the following chains were created:

We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])), COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) which results in the following constraint:
(13)    (>(x0[2], 0)=TRUE∧567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR))))=567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR))))∧java.lang.Object(x1[2])=java.lang.Object(x1[3]) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥))

We simplified constraint (13) using rules (I), (II), (IV), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(14)    (>(x0[2], 0)=TRUE ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)Bound*bni_20] + [(-1)bni_20]x1[2] + [bni_20]x0[2] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)Bound*bni_20] + [(-1)bni_20]x1[2] + [bni_20]x0[2] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)Bound*bni_20] + [(-1)bni_20]x1[2] + [bni_20]x0[2] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)bni_20] = 0∧[(-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (18) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(19)    (x0[2] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)bni_20] = 0∧[(-1)Bound*bni_20 + bni_20] + [bni_20]x0[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) the following chains were created:

We consider the chain COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) which results in the following constraint:
(20)    (COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))∧(U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) the following chains were created:

We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))), COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) which results in the following constraint:
(25)    (>(x0[4], 0)=TRUE∧567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4])))=567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5])))∧java.lang.Object(CyclicList(x1[4]))=java.lang.Object(CyclicList(x1[5])) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥))

We simplified constraint (25) using rules (I), (II), (IV) which results in the following new constraint:
(26)    (>(x0[4], 0)=TRUE ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(27)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x1[4] + [bni_24]x0[4] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(28)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x1[4] + [bni_24]x0[4] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x1[4] + [bni_24]x0[4] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(30)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)bni_24] = 0∧[(-1)Bound*bni_24] + [bni_24]x0[4] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(31)    (x0[4] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)bni_24] = 0∧[(-1)Bound*bni_24 + bni_24] + [bni_24]x0[4] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), x2), java.lang.Object(CyclicList(x1))) the following chains were created:

We consider the chain COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) which results in the following constraint:
(32)    (COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5])))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5])))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))∧(U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥))

We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(36)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) the following chains were created:

We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))), COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) which results in the following constraint:
(37)    (>(x0[6], 0)=TRUE∧567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR))))=567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥))

We simplified constraint (37) using rules (I), (II), (IV), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(38)    (>(x0[6], 0)=TRUE ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥))

We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(39)    (x0[6] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)

We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(40)    (x0[6] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)

We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(41)    (x0[6] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)

We simplified constraint (41) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(42)    (x0[6] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) the following chains were created:

We consider the chain COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) which results in the following constraint:
(43)    (COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))∧(U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥))

We simplified constraint (43) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(44)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(-1)bso_31] ≥ 0)

We simplified constraint (44) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(45)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(-1)bso_31] ≥ 0)

We simplified constraint (45) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(46)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(-1)bso_31] ≥ 0)

We simplified constraint (46) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(47)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧0 = 0∧[(-1)bso_31] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) → COND_567_1_MAIN_INVOKEMETHOD(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2))
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)bni_16] = 0∧0 = 0∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x0[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)
COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), x3), java.lang.Object(x2))
- ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1))
- (x0[2] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)bni_20] = 0∧[(-1)Bound*bni_20 + bni_20] + [bni_20]x0[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)
COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1))
- ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1)))
- (x0[4] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)bni_24] = 0∧[(-1)Bound*bni_24 + bni_24] + [bni_24]x0[4] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)
COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), x2), java.lang.Object(CyclicList(x1)))
- ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))
- (x0[6] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)
COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))
- ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧0 = 0∧[(-1)bso_31] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(567_1_MAIN_INVOKEMETHOD(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(567_0_get_Load(x₁, x₂)) = [-1] + [-1]x₁
POL(java.lang.Object(x₁)) = x₁
POL(CyclicList(x₁)) = x₁
POL(COND_567_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]
POL(EOR) = [-1]
POL(COND_567_1_MAIN_INVOKEMETHOD1(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(COND_567_1_MAIN_INVOKEMETHOD2(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(COND_567_1_MAIN_INVOKEMETHOD3(x₁, x₂, x₃)) = [-1] + [-1]x₂

The following pairs are in P_>:

COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))
COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

The following pairs are in P_bound:

567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

The following pairs are in P_≥:

567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

There are no usable rules.

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(x0[0] > 0, 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))
(1): COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[1] + -1, x3[1]), java.lang.Object(x2[1]))
(2): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(x0[2] > 0, 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
(3): COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
(4): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(x0[4] > 0, 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
(5): COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[5] + -1, x2[5]), java.lang.Object(CyclicList(x1[5])))
(7): COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

(1) -> (0), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(x2[0])))

(5) -> (0), if ((567_0_get_Load(x0[5] + -1, x2[5]) →^* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(CyclicList(x1[5])) →^* java.lang.Object(x2[0])))

(1) -> (2), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(x1[2])))

(1) -> (4), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(CyclicList(x1[4]))))

(5) -> (4), if ((567_0_get_Load(x0[5] + -1, x2[5]) →^* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(CyclicList(x1[5])) →^* java.lang.Object(CyclicList(x1[4]))))

The set Q is empty.

(8) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(5): COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[5] + -1, x2[5]), java.lang.Object(CyclicList(x1[5])))
(4): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(x0[4] > 0, 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
(3): COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
(2): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(x0[2] > 0, 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
(1): COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[1] + -1, x3[1]), java.lang.Object(x2[1]))
(0): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(x0[0] > 0, 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))

(1) -> (0), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(x2[0])))

(5) -> (0), if ((567_0_get_Load(x0[5] + -1, x2[5]) →^* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(CyclicList(x1[5])) →^* java.lang.Object(x2[0])))

(1) -> (2), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(x1[2])))

(1) -> (4), if ((567_0_get_Load(x0[1] + -1, x3[1]) →^* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x2[1]) →^* java.lang.Object(CyclicList(x1[4]))))

(5) -> (4), if ((567_0_get_Load(x0[5] + -1, x2[5]) →^* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(CyclicList(x1[5])) →^* java.lang.Object(CyclicList(x1[4]))))

The set Q is empty.

(10) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) the following chains were created:

We consider the chain COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) which results in the following constraint:
(1)    (COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5])))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5])))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))∧(U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[(-1)bso_17] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[(-1)bso_17] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[(-1)bso_17] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) the following chains were created:

We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))), COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) which results in the following constraint:
(6)    (>(x0[4], 0)=TRUE∧567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4])))=567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5])))∧java.lang.Object(CyclicList(x1[4]))=java.lang.Object(CyclicList(x1[5])) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥))

We simplified constraint (6) using rules (I), (II), (IV) which results in the following new constraint:
(7)    (>(x0[4], 0)=TRUE ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧0 = 0∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (x0[4] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) the following chains were created:

We consider the chain COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) which results in the following constraint:
(13)    (COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))∧(U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥))

We simplified constraint (13) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(14)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[(-1)bso_21] ≥ 0)

We simplified constraint (14) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(15)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[(-1)bso_21] ≥ 0)

We simplified constraint (15) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(16)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[(-1)bso_21] ≥ 0)

We simplified constraint (16) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(17)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_21] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) the following chains were created:

We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])), COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) which results in the following constraint:
(18)    (>(x0[2], 0)=TRUE∧567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR))))=567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR))))∧java.lang.Object(x1[2])=java.lang.Object(x1[3]) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥))

We simplified constraint (18) using rules (I), (II), (IV), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(19)    (>(x0[2], 0)=TRUE ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥))

We simplified constraint (19) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(20)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (20) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(21)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (21) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(22)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (22) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(23)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧0 = 0∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (23) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(24)    (x0[2] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧0 = 0∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) the following chains were created:

We consider the chain COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) which results in the following constraint:
(25)    (COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1]))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1]))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))∧(U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥))

We simplified constraint (25) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(26)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[(-1)bso_25] ≥ 0)

We simplified constraint (26) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(27)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[(-1)bso_25] ≥ 0)

We simplified constraint (27) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(28)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[(-1)bso_25] ≥ 0)

We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(29)    ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) the following chains were created:

We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])), COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) which results in the following constraint:
(30)    (>(x0[0], 0)=TRUE∧567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0])))=567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1])))∧java.lang.Object(x2[0])=java.lang.Object(x2[1]) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥))

We simplified constraint (30) using rules (I), (II), (IV) which results in the following new constraint:
(31)    (>(x0[0], 0)=TRUE ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))∧(U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥))

We simplified constraint (31) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(32)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (32) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(33)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (33) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(34)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (34) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(35)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (35) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(36)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧0 = 0∧0 = 0∧[(2)bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))
- ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
- (x0[4] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)
COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
- ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_21] ≥ 0)
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
- (x0[2] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧0 = 0∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)
COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))
- ((U^Increasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧0 = 0∧0 = 0∧[(2)bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_567_1_MAIN_INVOKEMETHOD2(x₁, x₂, x₃)) = [-1] + [-1]x₂
POL(567_0_get_Load(x₁, x₂)) = [-1] + [-1]x₁
POL(java.lang.Object(x₁)) = x₁
POL(CyclicList(x₁)) = x₁
POL(567_1_MAIN_INVOKEMETHOD(x₁, x₂)) = [-1]x₁
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(COND_567_1_MAIN_INVOKEMETHOD1(x₁, x₂, x₃)) = [-1] + [-1]x₂
POL(EOR) = [-1]
POL(COND_567_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₂

The following pairs are in P_>:

567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))

The following pairs are in P_bound:

567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))

The following pairs are in P_≥:

COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))
COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))

There are no usable rules.

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(12) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(13) TRUE

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))) → COND_160_1_MAIN_INVOKEMETHOD(x0[0] > 0, 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))
(1): COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[1] + -1, java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))

(0) -> (1), if ((x0[0] > 0 →^* TRUE)∧(160_0_create_Load(x0[0], java.lang.Object(x1[0])) →^* 160_0_create_Load(x0[1], java.lang.Object(x1[1])))∧(java.lang.Object(ARRAY(x2[0], x3[0])) →^* java.lang.Object(ARRAY(x2[1], x3[1]))))

(1) -> (0), if ((160_0_create_Load(x0[1] + -1, java.lang.Object(CyclicList)) →^* 160_0_create_Load(x0[0], java.lang.Object(x1[0])))∧(java.lang.Object(ARRAY(x2[1], x3[1])) →^* java.lang.Object(ARRAY(x2[0], x3[0]))))

The set Q is empty.

(15) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0, 0), 160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) the following chains were created:

We consider the chain 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))), COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1]))) which results in the following constraint:
(1)    (>(x0[0], 0)=TRUE∧160_0_create_Load(x0[0], java.lang.Object(x1[0]))=160_0_create_Load(x0[1], java.lang.Object(x1[1]))∧java.lang.Object(ARRAY(x2[0], x3[0]))=java.lang.Object(ARRAY(x2[1], x3[1])) ⇒ 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))≥NonInfC∧160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))≥COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))∧(U^Increasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (>(x0[0], 0)=TRUE ⇒ 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))≥NonInfC∧160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))≥COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))∧(U^Increasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧[(3)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧[(3)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧[(3)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧0 = 0∧[(3)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧0 = 0∧[(-1)bso_14] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧0 = 0∧[(4)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧0 = 0∧[(-1)bso_14] ≥ 0)

For Pair COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0, -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2, x3))) the following chains were created:

We consider the chain COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1]))) which results in the following constraint:
(8)    (COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1])))≥NonInfC∧COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1])))≥160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))∧(U^Increasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    ((U^Increasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧[1 + (-1)bso_16] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    ((U^Increasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧[1 + (-1)bso_16] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    ((U^Increasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧[1 + (-1)bso_16] ≥ 0)

We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(12)    ((U^Increasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0, 0), 160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3)))
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧0 = 0∧[(4)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧0 = 0∧[(-1)bso_14] ≥ 0)
COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0, -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2, x3)))
- ((U^Increasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(160_1_MAIN_INVOKEMETHOD(x₁, x₂)) = [2] + [-1]x₁
POL(160_0_create_Load(x₁, x₂)) = [-1] + [-1]x₁
POL(java.lang.Object(x₁)) = x₁
POL(ARRAY(x₁, x₂)) = [-1]
POL(COND_160_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = [2] + [-1]x₂
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]
POL(CyclicList) = [-1]

The following pairs are in P_>:

COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))

The following pairs are in P_bound:

160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))

The following pairs are in P_≥:

160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))

There are no usable rules.

(16) Complex Obligation (AND)

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(18) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(19) TRUE

(20) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[1] + -1, java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))

The set Q is empty.

(21) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) JBC2FIG (SOUND transformation)

(2) Obligation:

(3) FIGtoITRSProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) IDPNonInfProof (SOUND transformation)

(7) Obligation:

(8) IDependencyGraphProof (EQUIVALENT transformation)

(9) Obligation:

(10) IDPNonInfProof (SOUND transformation)

(11) Obligation:

(12) IDependencyGraphProof (EQUIVALENT transformation)

(13) TRUE

(14) Obligation:

(15) IDPNonInfProof (SOUND transformation)

(16) Complex Obligation (AND)

(17) Obligation:

(18) IDependencyGraphProof (EQUIVALENT transformation)

(19) TRUE

(20) Obligation:

(21) IDependencyGraphProof (EQUIVALENT transformation)

(22) TRUE